Metamath Blueprint : AKS (PRIMES is in P)

Theorem akslb

Draft
$e |- ( ph -> N e. ( ZZ>= ` ; ; ; ; 1 0 0 0 0 ) ) $.
$e |- ( ph -> R e. ( 1 ... ( |^ ` ( ( 2 log N ) ^ 5 ) ) ) ) $.
$e |- ( ph -> A e. ( 1 ... ( |_ ` ( ( sqrt ` ( phi ` R )  ) x. ( 2 log N )  )  ) ) ) $.
$p |- ( ph -> A < N ) $.
Lemma 2.3 from ~ https://www3.nd.edu/%7eandyp/notes/AKS.pdf

Eliminate lower values of n: the hypotheses of Theorem 2.2 only need to be checked for fairly large n.